mcsta

mcsta/modest mcsta crowds.jani -E TotalRuns=6,CrowdSize=20 --props positive -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --p0 --p1

crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 40 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 10291282 states for TotalRuns=6, CrowdSize=20.

Peak memory usage: 3439 MB
Analysis results for crowds.jani
Experiment TotalRuns=6, CrowdSize=20

+ State space exploration
  State size:  40 bytes
  States:      10291282
  Transitions: 10291282
  Branches:    37068802
  Rate:        398115 states/s
  Time:        27.2 s

+ Property positive
  Probability: 0.1204761609299478
  Bounds:      [0.1204761609299478, 1]
  Time:        9.5 s

  + Precomputations
    Min. prob. 0 states:          8587502
    Time for min. prob. 0 states: 2.4 s
    Min. prob. 1 states:          21252
    Time for min. prob. 1 states: 0.4 s

  + Essential states
    Iterations:       2
    Essential states: 1275122
    Transitions:      1275122
    Branches:         10200962
    Time:             1.3 s

  + Value iteration
    Final error: 8.778542281008603E-07
    Iterations:  63
    Time:        5.4 s

Exported results to file "/out.txt".	

The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.